This present disclosure relates generally to formal verification of circuit designs, and more particularly to formal verification methods of verifying data access and data propagation paths in multi-system circuits.
Devices such as mobile phones, gaming consoles, and set top boxes often include multiple computing devices that store, share, or otherwise access sensitive data. For example, sensitive data, such as encryption and decryption keys, may be designed to be read from secure locations within a computing device and sent to other secure functional components through secure channels within the device. Handling of sensitive data has related security requirements, which generally specify that (1) secure data and control information should not reach non-secure areas of the computing device and (2) non-secure data and control information should not propagate to secure areas of the computing device or interfere with secure operations performed by the computing device. The role of initiators (e.g., masters) and receivers (e.g., slaves) regarding one or a combination of data and control information are important when analyzing these requirements. Analysis regarding whether secure data and control information has passed through an encryption path or not is also important.
Overall, the process of integrating multiple intellectual property (IP) functional components to create multi-system circuits sometimes provides an unexpected path to secure areas of the computing device. The addition of test logic and associated test ports may create a path by which secure data may be accessed by an interface external to the computing device. The resulting path may create a security leak (i.e. violation to requirement 1 above) or an illegal modification or interference on a secure area (i.e. violation to requirement 2 above). Current techniques used to verify that a design is free from data security leaks or unintentional pathways creating unauthorized data access are insufficient.